/*    This file is part of unfy.
 *
 *    Unfy is free software: you can redistribute it and/or modify
 *    it under the terms of the GNU Lesser General Public License as published by
 *    the Free Software Foundation, either version 3 of the License, or
 *    (at your option) any later version.
 *
 *    Unfy is distributed in the hope that it will be useful,
 *    but WITHOUT ANY WARRANTY; without even the implied warranty of
 *    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *    GNU Lesser General Public License for more details.
 *
 *    You should have received a copy of the GNU Lesser General Public License
 *    along with unfy.  If not, see <http://www.gnu.org/licenses/>.
 */

#include <rid.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

#define STYLE_9
#include <fn85.h>
#include <rid_fn85.h>

#include "../unfy.h"
#include "../unfp.h"

void
try_unify(Unfy_term *term1, Unfy_term *term2, Unfy_recycle *rec)
{
	Unfy_info info;
	Unfy_term *bound;

	unfy_info_init(&info, term1, term2);

	/* Switch between assuming variables from term1 are independent from
	 * variables of the same name in term2. This type of semantic structure
	 * assumption is preserved, but only one term can be used for
	 * extraction of data (since only it maintains the names agreed to mean
	 * something particular since the other term has those names changed).
	 * In this case, this would be term1. This mechanism is useful for
	 * building recursive rule based systems.
	 */
	if (unfy_term_revar(term2, &info.rbind, rec) < 0 ||
	    unfy_term_bind_set(term2, info.rbind, rec) < 0) {
		unfy_recycle_bind(rec, info.rbind);
		printf("Failed to rename same variables in second term.\n");
		return;
	}

	unfy_recycle_bind(rec, info.rbind);
	info.rbind = NULL;

	/* Switch between testing unification or structural sameness */
	switch (unfy_term_same(&info, rec)) {
	/* switch (unfy_unify(&info, rec)) { */
	case UNFY_YES:
		printf("YES: ");

		if (!(bound = unfy_term_bind(term1, info.lbind, rec))) {
			printf("error binding.\n");
		} else {
			unfp_term_print(bound);
			printf("\n");
			unfy_recycle_term(rec, bound);
		}

		printf("LEFT BINDS:\n");
		unfp_binds_print(info.lbind, 1);
		printf("RIGHT BINDS:\n");
		unfp_binds_print(info.rbind, 1);
		break;
	case UNFY_NO:
		printf("NO\n\n");
		switch (info.rsn) {
		case UNFY_RSN_OKAY:
			printf("How did this happen?!\n");
			break;
		case UNFY_RSN_VAL:
			printf("Values differ\n");
			break;
		case UNFY_RSN_TYPE:
			printf("Types differ\n");
			break;
		case UNFY_RSN_LEN:
			printf("Lists differ in length\n");
			break;
		case UNFY_RSN_SELF:
			printf("Varaible cannot be in itself\n");
			break;
		}

		printf("LEFT TERM:\n\t");
		unfp_term_print(info.left);
		printf("\n");

		if (info.lvar) {
			printf("In var:\n\t");
			unfp_term_print(info.lvar);
			printf("\n");
		}

		printf("RIGHT TERM:\n\t");
		unfp_term_print(info.right);
		printf("\n");

		if (info.rvar) {
			printf("In var:\n\t");
			unfp_term_print(info.rvar);
			printf("\n");
		}

		break;
	case UNFY_ERR:
		printf("ERR\n\n");
		break;
	}

	unfy_recycle_bind(rec, info.lbind);
	unfy_recycle_bind(rec, info.rbind);
}

void
repl(void)
{
	Unfy_recycle rec;
        char *str = NULL;
	size_t n = 0;
	const char *error;

	unfy_recycle_init(&rec);

	while (1) {
		size_t pos = 0;
		Unfy_term *term1;
		Unfy_term *term2;

		printf("* ");

		if (getline(&str, &n, stdin) < 0) {
			printf("Closing repl\n");
			break;
		}

		if (!(term1 = unfp_term_parse(str, &pos, &error, &rec))) {
			printf("%s at %zu\n", error, pos);
			continue;
		}

		if (unfp_space(str + pos, &pos, &error)) {
			printf("%s at %zu\n", error, pos);
			unfy_recycle_term(&rec, term1);
			continue;
		}

		if (!(term2 = unfp_term_parse(str + pos, &pos,
					      &error, &rec))) {
			printf("%s at %zu\n", error, pos);
			unfy_recycle_term(&rec, term1);
		        continue;
		}

		try_unify(term1, term2, &rec);
		unfy_recycle_term(&rec, term1);
		unfy_recycle_term(&rec, term2);
	}

	unfy_recycle_empty(&rec);
	free(str);
}

int
main(int argc, char *argv[])
{
	repl();
	return 0;
}
